x, y:(Top List), b:. null(if b then x else y fi ) = if b then null(x) else null(y) fi    

latex

ProofTree

Definitions	t  T, Top, x:A. B(x), null(as), b, A, b, , , P  Q, P & Q, P  Q, Unit
Lemmas	eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, not wf, assert wf, null wf, top wf